(set-logic QF_BV)
(set-info :source "
We verify the correctness of the \"next power of 2 algorithm\"
from the book \"hacker's delight\" (Warren Jr., Henry).

Algorithm:
int next_power_of_2 (int x)
{
  int i;
  x--;
  for (i = 1; i < sizeof(int) * 8; i = i * 2)
  x = x | (x >> i)
  return x + 1;
}

Bit-width: 128

Contributed by Robert Brummayer (robert.brummayer@gmail.com).
")
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun x () (_ BitVec 128))
(assert (let ((?v_0 (bvadd x (bvadd (bvnot (_ bv1 128)) (_ bv1 128)))) (?v_2 ((_ zero_extend 121) (_ bv1 7)))) (let ((?v_1 (bvnot ?v_0))) (let ((?v_3 (bvand ?v_1 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_0)) (bvnot (bvlshr ?v_1 ?v_2)) (bvlshr ?v_0 ?v_2)))))) (let ((?v_4 (bvnot ?v_3)) (?v_5 ((_ zero_extend 121) (_ bv2 7)))) (let ((?v_6 (bvand ?v_3 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_4)) (bvnot (bvlshr ?v_3 ?v_5)) (bvlshr ?v_4 ?v_5)))))) (let ((?v_7 (bvnot ?v_6)) (?v_8 ((_ zero_extend 121) (_ bv3 7)))) (let ((?v_9 (bvand ?v_6 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_7)) (bvnot (bvlshr ?v_6 ?v_8)) (bvlshr ?v_7 ?v_8)))))) (let ((?v_10 (bvnot ?v_9)) (?v_11 ((_ zero_extend 121) (_ bv4 7)))) (let ((?v_12 (bvand ?v_9 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_10)) (bvnot (bvlshr ?v_9 ?v_11)) (bvlshr ?v_10 ?v_11)))))) (let ((?v_13 (bvnot ?v_12)) (?v_14 ((_ zero_extend 121) (_ bv5 7)))) (let ((?v_15 (bvand ?v_12 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_13)) (bvnot (bvlshr ?v_12 ?v_14)) (bvlshr ?v_13 ?v_14)))))) (let ((?v_16 (bvnot ?v_15)) (?v_17 ((_ zero_extend 121) (_ bv6 7)))) (let ((?v_18 (bvand ?v_15 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_16)) (bvnot (bvlshr ?v_15 ?v_17)) (bvlshr ?v_16 ?v_17)))))) (let ((?v_19 (bvnot ?v_18)) (?v_20 ((_ zero_extend 121) (_ bv7 7)))) (let ((?v_21 (bvand ?v_18 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_19)) (bvnot (bvlshr ?v_18 ?v_20)) (bvlshr ?v_19 ?v_20)))))) (let ((?v_22 (bvnot ?v_21)) (?v_23 ((_ zero_extend 121) (_ bv8 7)))) (let ((?v_24 (bvand ?v_21 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_22)) (bvnot (bvlshr ?v_21 ?v_23)) (bvlshr ?v_22 ?v_23)))))) (let ((?v_25 (bvnot ?v_24)) (?v_26 ((_ zero_extend 121) (_ bv9 7)))) (let ((?v_27 (bvand ?v_24 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_25)) (bvnot (bvlshr ?v_24 ?v_26)) (bvlshr ?v_25 ?v_26)))))) (let ((?v_28 (bvnot ?v_27)) (?v_29 ((_ zero_extend 121) (_ bv10 7)))) (let ((?v_30 (bvand ?v_27 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_28)) (bvnot (bvlshr ?v_27 ?v_29)) (bvlshr ?v_28 ?v_29)))))) (let ((?v_31 (bvnot ?v_30)) (?v_32 ((_ zero_extend 121) (_ bv11 7)))) (let ((?v_33 (bvand ?v_30 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_31)) (bvnot (bvlshr ?v_30 ?v_32)) (bvlshr ?v_31 ?v_32)))))) (let ((?v_34 (bvnot ?v_33)) (?v_35 ((_ zero_extend 121) (_ bv12 7)))) (let ((?v_36 (bvand ?v_33 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_34)) (bvnot (bvlshr ?v_33 ?v_35)) (bvlshr ?v_34 ?v_35)))))) (let ((?v_37 (bvnot ?v_36)) (?v_38 ((_ zero_extend 121) (_ bv13 7)))) (let ((?v_39 (bvand ?v_36 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_37)) (bvnot (bvlshr ?v_36 ?v_38)) (bvlshr ?v_37 ?v_38)))))) (let ((?v_40 (bvnot ?v_39)) (?v_41 ((_ zero_extend 121) (_ bv14 7)))) (let ((?v_42 (bvand ?v_39 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_40)) (bvnot (bvlshr ?v_39 ?v_41)) (bvlshr ?v_40 ?v_41)))))) (let ((?v_43 (bvnot ?v_42)) (?v_44 ((_ zero_extend 121) (_ bv15 7)))) (let ((?v_45 (bvand ?v_42 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_43)) (bvnot (bvlshr ?v_42 ?v_44)) (bvlshr ?v_43 ?v_44)))))) (let ((?v_46 (bvnot ?v_45)) (?v_47 ((_ zero_extend 121) (_ bv16 7)))) (let ((?v_48 (bvand ?v_45 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_46)) (bvnot (bvlshr ?v_45 ?v_47)) (bvlshr ?v_46 ?v_47)))))) (let ((?v_49 (bvnot ?v_48)) (?v_50 ((_ zero_extend 121) (_ bv17 7)))) (let ((?v_51 (bvand ?v_48 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_49)) (bvnot (bvlshr ?v_48 ?v_50)) (bvlshr ?v_49 ?v_50)))))) (let ((?v_52 (bvnot ?v_51)) (?v_53 ((_ zero_extend 121) (_ bv18 7)))) (let ((?v_54 (bvand ?v_51 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_52)) (bvnot (bvlshr ?v_51 ?v_53)) (bvlshr ?v_52 ?v_53)))))) (let ((?v_55 (bvnot ?v_54)) (?v_56 ((_ zero_extend 121) (_ bv19 7)))) (let ((?v_57 (bvand ?v_54 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_55)) (bvnot (bvlshr ?v_54 ?v_56)) (bvlshr ?v_55 ?v_56)))))) (let ((?v_58 (bvnot ?v_57)) (?v_59 ((_ zero_extend 121) (_ bv20 7)))) (let ((?v_60 (bvand ?v_57 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_58)) (bvnot (bvlshr ?v_57 ?v_59)) (bvlshr ?v_58 ?v_59)))))) (let ((?v_61 (bvnot ?v_60)) (?v_62 ((_ zero_extend 121) (_ bv21 7)))) (let ((?v_63 (bvand ?v_60 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_61)) (bvnot (bvlshr ?v_60 ?v_62)) (bvlshr ?v_61 ?v_62)))))) (let ((?v_64 (bvnot ?v_63)) (?v_65 ((_ zero_extend 121) (_ bv22 7)))) (let ((?v_66 (bvand ?v_63 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_64)) (bvnot (bvlshr ?v_63 ?v_65)) (bvlshr ?v_64 ?v_65)))))) (let ((?v_67 (bvnot ?v_66)) (?v_68 ((_ zero_extend 121) (_ bv23 7)))) (let ((?v_69 (bvand ?v_66 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_67)) (bvnot (bvlshr ?v_66 ?v_68)) (bvlshr ?v_67 ?v_68)))))) (let ((?v_70 (bvnot ?v_69)) (?v_71 ((_ zero_extend 121) (_ bv24 7)))) (let ((?v_72 (bvand ?v_69 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_70)) (bvnot (bvlshr ?v_69 ?v_71)) (bvlshr ?v_70 ?v_71)))))) (let ((?v_73 (bvnot ?v_72)) (?v_74 ((_ zero_extend 121) (_ bv25 7)))) (let ((?v_75 (bvand ?v_72 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_73)) (bvnot (bvlshr ?v_72 ?v_74)) (bvlshr ?v_73 ?v_74)))))) (let ((?v_76 (bvnot ?v_75)) (?v_77 ((_ zero_extend 121) (_ bv26 7)))) (let ((?v_78 (bvand ?v_75 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_76)) (bvnot (bvlshr ?v_75 ?v_77)) (bvlshr ?v_76 ?v_77)))))) (let ((?v_79 (bvnot ?v_78)) (?v_80 ((_ zero_extend 121) (_ bv27 7)))) (let ((?v_81 (bvand ?v_78 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_79)) (bvnot (bvlshr ?v_78 ?v_80)) (bvlshr ?v_79 ?v_80)))))) (let ((?v_82 (bvnot ?v_81)) (?v_83 ((_ zero_extend 121) (_ bv28 7)))) (let ((?v_84 (bvand ?v_81 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_82)) (bvnot (bvlshr ?v_81 ?v_83)) (bvlshr ?v_82 ?v_83)))))) (let ((?v_85 (bvnot ?v_84)) (?v_86 ((_ zero_extend 121) (_ bv29 7)))) (let ((?v_87 (bvand ?v_84 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_85)) (bvnot (bvlshr ?v_84 ?v_86)) (bvlshr ?v_85 ?v_86)))))) (let ((?v_88 (bvnot ?v_87)) (?v_89 ((_ zero_extend 121) (_ bv30 7)))) (let ((?v_90 (bvand ?v_87 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_88)) (bvnot (bvlshr ?v_87 ?v_89)) (bvlshr ?v_88 ?v_89)))))) (let ((?v_91 (bvnot ?v_90)) (?v_92 ((_ zero_extend 121) (_ bv31 7)))) (let ((?v_93 (bvand ?v_90 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_91)) (bvnot (bvlshr ?v_90 ?v_92)) (bvlshr ?v_91 ?v_92)))))) (let ((?v_94 (bvnot ?v_93)) (?v_95 ((_ zero_extend 121) (_ bv32 7)))) (let ((?v_96 (bvand ?v_93 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_94)) (bvnot (bvlshr ?v_93 ?v_95)) (bvlshr ?v_94 ?v_95)))))) (let ((?v_97 (bvnot ?v_96)) (?v_98 ((_ zero_extend 121) (_ bv33 7)))) (let ((?v_99 (bvand ?v_96 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_97)) (bvnot (bvlshr ?v_96 ?v_98)) (bvlshr ?v_97 ?v_98)))))) (let ((?v_100 (bvnot ?v_99)) (?v_101 ((_ zero_extend 121) (_ bv34 7)))) (let ((?v_102 (bvand ?v_99 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_100)) (bvnot (bvlshr ?v_99 ?v_101)) (bvlshr ?v_100 ?v_101)))))) (let ((?v_103 (bvnot ?v_102)) (?v_104 ((_ zero_extend 121) (_ bv35 7)))) (let ((?v_105 (bvand ?v_102 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_103)) (bvnot (bvlshr ?v_102 ?v_104)) (bvlshr ?v_103 ?v_104)))))) (let ((?v_106 (bvnot ?v_105)) (?v_107 ((_ zero_extend 121) (_ bv36 7)))) (let ((?v_108 (bvand ?v_105 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_106)) (bvnot (bvlshr ?v_105 ?v_107)) (bvlshr ?v_106 ?v_107)))))) (let ((?v_109 (bvnot ?v_108)) (?v_110 ((_ zero_extend 121) (_ bv37 7)))) (let ((?v_111 (bvand ?v_108 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_109)) (bvnot (bvlshr ?v_108 ?v_110)) (bvlshr ?v_109 ?v_110)))))) (let ((?v_112 (bvnot ?v_111)) (?v_113 ((_ zero_extend 121) (_ bv38 7)))) (let ((?v_114 (bvand ?v_111 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_112)) (bvnot (bvlshr ?v_111 ?v_113)) (bvlshr ?v_112 ?v_113)))))) (let ((?v_115 (bvnot ?v_114)) (?v_116 ((_ zero_extend 121) (_ bv39 7)))) (let ((?v_117 (bvand ?v_114 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_115)) (bvnot (bvlshr ?v_114 ?v_116)) (bvlshr ?v_115 ?v_116)))))) (let ((?v_118 (bvnot ?v_117)) (?v_119 ((_ zero_extend 121) (_ bv40 7)))) (let ((?v_120 (bvand ?v_117 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_118)) (bvnot (bvlshr ?v_117 ?v_119)) (bvlshr ?v_118 ?v_119)))))) (let ((?v_121 (bvnot ?v_120)) (?v_122 ((_ zero_extend 121) (_ bv41 7)))) (let ((?v_123 (bvand ?v_120 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_121)) (bvnot (bvlshr ?v_120 ?v_122)) (bvlshr ?v_121 ?v_122)))))) (let ((?v_124 (bvnot ?v_123)) (?v_125 ((_ zero_extend 121) (_ bv42 7)))) (let ((?v_126 (bvand ?v_123 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_124)) (bvnot (bvlshr ?v_123 ?v_125)) (bvlshr ?v_124 ?v_125)))))) (let ((?v_127 (bvnot ?v_126)) (?v_128 ((_ zero_extend 121) (_ bv43 7)))) (let ((?v_129 (bvand ?v_126 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_127)) (bvnot (bvlshr ?v_126 ?v_128)) (bvlshr ?v_127 ?v_128)))))) (let ((?v_130 (bvnot ?v_129)) (?v_131 ((_ zero_extend 121) (_ bv44 7)))) (let ((?v_132 (bvand ?v_129 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_130)) (bvnot (bvlshr ?v_129 ?v_131)) (bvlshr ?v_130 ?v_131)))))) (let ((?v_133 (bvnot ?v_132)) (?v_134 ((_ zero_extend 121) (_ bv45 7)))) (let ((?v_135 (bvand ?v_132 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_133)) (bvnot (bvlshr ?v_132 ?v_134)) (bvlshr ?v_133 ?v_134)))))) (let ((?v_136 (bvnot ?v_135)) (?v_137 ((_ zero_extend 121) (_ bv46 7)))) (let ((?v_138 (bvand ?v_135 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_136)) (bvnot (bvlshr ?v_135 ?v_137)) (bvlshr ?v_136 ?v_137)))))) (let ((?v_139 (bvnot ?v_138)) (?v_140 ((_ zero_extend 121) (_ bv47 7)))) (let ((?v_141 (bvand ?v_138 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_139)) (bvnot (bvlshr ?v_138 ?v_140)) (bvlshr ?v_139 ?v_140)))))) (let ((?v_142 (bvnot ?v_141)) (?v_143 ((_ zero_extend 121) (_ bv48 7)))) (let ((?v_144 (bvand ?v_141 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_142)) (bvnot (bvlshr ?v_141 ?v_143)) (bvlshr ?v_142 ?v_143)))))) (let ((?v_145 (bvnot ?v_144)) (?v_146 ((_ zero_extend 121) (_ bv49 7)))) (let ((?v_147 (bvand ?v_144 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_145)) (bvnot (bvlshr ?v_144 ?v_146)) (bvlshr ?v_145 ?v_146)))))) (let ((?v_148 (bvnot ?v_147)) (?v_149 ((_ zero_extend 121) (_ bv50 7)))) (let ((?v_150 (bvand ?v_147 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_148)) (bvnot (bvlshr ?v_147 ?v_149)) (bvlshr ?v_148 ?v_149)))))) (let ((?v_151 (bvnot ?v_150)) (?v_152 ((_ zero_extend 121) (_ bv51 7)))) (let ((?v_153 (bvand ?v_150 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_151)) (bvnot (bvlshr ?v_150 ?v_152)) (bvlshr ?v_151 ?v_152)))))) (let ((?v_154 (bvnot ?v_153)) (?v_155 ((_ zero_extend 121) (_ bv52 7)))) (let ((?v_156 (bvand ?v_153 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_154)) (bvnot (bvlshr ?v_153 ?v_155)) (bvlshr ?v_154 ?v_155)))))) (let ((?v_157 (bvnot ?v_156)) (?v_158 ((_ zero_extend 121) (_ bv53 7)))) (let ((?v_159 (bvand ?v_156 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_157)) (bvnot (bvlshr ?v_156 ?v_158)) (bvlshr ?v_157 ?v_158)))))) (let ((?v_160 (bvnot ?v_159)) (?v_161 ((_ zero_extend 121) (_ bv54 7)))) (let ((?v_162 (bvand ?v_159 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_160)) (bvnot (bvlshr ?v_159 ?v_161)) (bvlshr ?v_160 ?v_161)))))) (let ((?v_163 (bvnot ?v_162)) (?v_164 ((_ zero_extend 121) (_ bv55 7)))) (let ((?v_165 (bvand ?v_162 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_163)) (bvnot (bvlshr ?v_162 ?v_164)) (bvlshr ?v_163 ?v_164)))))) (let ((?v_166 (bvnot ?v_165)) (?v_167 ((_ zero_extend 121) (_ bv56 7)))) (let ((?v_168 (bvand ?v_165 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_166)) (bvnot (bvlshr ?v_165 ?v_167)) (bvlshr ?v_166 ?v_167)))))) (let ((?v_169 (bvnot ?v_168)) (?v_170 ((_ zero_extend 121) (_ bv57 7)))) (let ((?v_171 (bvand ?v_168 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_169)) (bvnot (bvlshr ?v_168 ?v_170)) (bvlshr ?v_169 ?v_170)))))) (let ((?v_172 (bvnot ?v_171)) (?v_173 ((_ zero_extend 121) (_ bv58 7)))) (let ((?v_174 (bvand ?v_171 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_172)) (bvnot (bvlshr ?v_171 ?v_173)) (bvlshr ?v_172 ?v_173)))))) (let ((?v_175 (bvnot ?v_174)) (?v_176 ((_ zero_extend 121) (_ bv59 7)))) (let ((?v_177 (bvand ?v_174 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_175)) (bvnot (bvlshr ?v_174 ?v_176)) (bvlshr ?v_175 ?v_176)))))) (let ((?v_178 (bvnot ?v_177)) (?v_179 ((_ zero_extend 121) (_ bv60 7)))) (let ((?v_180 (bvand ?v_177 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_178)) (bvnot (bvlshr ?v_177 ?v_179)) (bvlshr ?v_178 ?v_179)))))) (let ((?v_181 (bvnot ?v_180)) (?v_182 ((_ zero_extend 121) (_ bv61 7)))) (let ((?v_183 (bvand ?v_180 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_181)) (bvnot (bvlshr ?v_180 ?v_182)) (bvlshr ?v_181 ?v_182)))))) (let ((?v_184 (bvnot ?v_183)) (?v_185 ((_ zero_extend 121) (_ bv62 7)))) (let ((?v_186 (bvand ?v_183 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_184)) (bvnot (bvlshr ?v_183 ?v_185)) (bvlshr ?v_184 ?v_185)))))) (let ((?v_187 (bvnot ?v_186)) (?v_188 ((_ zero_extend 121) (_ bv63 7)))) (let ((?v_189 (bvand ?v_186 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_187)) (bvnot (bvlshr ?v_186 ?v_188)) (bvlshr ?v_187 ?v_188)))))) (let ((?v_190 (bvnot ?v_189)) (?v_191 ((_ zero_extend 121) (_ bv64 7)))) (let ((?v_192 (bvand ?v_189 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_190)) (bvnot (bvlshr ?v_189 ?v_191)) (bvlshr ?v_190 ?v_191)))))) (let ((?v_193 (bvnot ?v_192)) (?v_194 ((_ zero_extend 121) (_ bv65 7)))) (let ((?v_195 (bvand ?v_192 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_193)) (bvnot (bvlshr ?v_192 ?v_194)) (bvlshr ?v_193 ?v_194)))))) (let ((?v_196 (bvnot ?v_195)) (?v_197 ((_ zero_extend 121) (_ bv66 7)))) (let ((?v_198 (bvand ?v_195 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_196)) (bvnot (bvlshr ?v_195 ?v_197)) (bvlshr ?v_196 ?v_197)))))) (let ((?v_199 (bvnot ?v_198)) (?v_200 ((_ zero_extend 121) (_ bv67 7)))) (let ((?v_201 (bvand ?v_198 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_199)) (bvnot (bvlshr ?v_198 ?v_200)) (bvlshr ?v_199 ?v_200)))))) (let ((?v_202 (bvnot ?v_201)) (?v_203 ((_ zero_extend 121) (_ bv68 7)))) (let ((?v_204 (bvand ?v_201 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_202)) (bvnot (bvlshr ?v_201 ?v_203)) (bvlshr ?v_202 ?v_203)))))) (let ((?v_205 (bvnot ?v_204)) (?v_206 ((_ zero_extend 121) (_ bv69 7)))) (let ((?v_207 (bvand ?v_204 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_205)) (bvnot (bvlshr ?v_204 ?v_206)) (bvlshr ?v_205 ?v_206)))))) (let ((?v_208 (bvnot ?v_207)) (?v_209 ((_ zero_extend 121) (_ bv70 7)))) (let ((?v_210 (bvand ?v_207 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_208)) (bvnot (bvlshr ?v_207 ?v_209)) (bvlshr ?v_208 ?v_209)))))) (let ((?v_211 (bvnot ?v_210)) (?v_212 ((_ zero_extend 121) (_ bv71 7)))) (let ((?v_213 (bvand ?v_210 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_211)) (bvnot (bvlshr ?v_210 ?v_212)) (bvlshr ?v_211 ?v_212)))))) (let ((?v_214 (bvnot ?v_213)) (?v_215 ((_ zero_extend 121) (_ bv72 7)))) (let ((?v_216 (bvand ?v_213 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_214)) (bvnot (bvlshr ?v_213 ?v_215)) (bvlshr ?v_214 ?v_215)))))) (let ((?v_217 (bvnot ?v_216)) (?v_218 ((_ zero_extend 121) (_ bv73 7)))) (let ((?v_219 (bvand ?v_216 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_217)) (bvnot (bvlshr ?v_216 ?v_218)) (bvlshr ?v_217 ?v_218)))))) (let ((?v_220 (bvnot ?v_219)) (?v_221 ((_ zero_extend 121) (_ bv74 7)))) (let ((?v_222 (bvand ?v_219 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_220)) (bvnot (bvlshr ?v_219 ?v_221)) (bvlshr ?v_220 ?v_221)))))) (let ((?v_223 (bvnot ?v_222)) (?v_224 ((_ zero_extend 121) (_ bv75 7)))) (let ((?v_225 (bvand ?v_222 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_223)) (bvnot (bvlshr ?v_222 ?v_224)) (bvlshr ?v_223 ?v_224)))))) (let ((?v_226 (bvnot ?v_225)) (?v_227 ((_ zero_extend 121) (_ bv76 7)))) (let ((?v_228 (bvand ?v_225 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_226)) (bvnot (bvlshr ?v_225 ?v_227)) (bvlshr ?v_226 ?v_227)))))) (let ((?v_229 (bvnot ?v_228)) (?v_230 ((_ zero_extend 121) (_ bv77 7)))) (let ((?v_231 (bvand ?v_228 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_229)) (bvnot (bvlshr ?v_228 ?v_230)) (bvlshr ?v_229 ?v_230)))))) (let ((?v_232 (bvnot ?v_231)) (?v_233 ((_ zero_extend 121) (_ bv78 7)))) (let ((?v_234 (bvand ?v_231 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_232)) (bvnot (bvlshr ?v_231 ?v_233)) (bvlshr ?v_232 ?v_233)))))) (let ((?v_235 (bvnot ?v_234)) (?v_236 ((_ zero_extend 121) (_ bv79 7)))) (let ((?v_237 (bvand ?v_234 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_235)) (bvnot (bvlshr ?v_234 ?v_236)) (bvlshr ?v_235 ?v_236)))))) (let ((?v_238 (bvnot ?v_237)) (?v_239 ((_ zero_extend 121) (_ bv80 7)))) (let ((?v_240 (bvand ?v_237 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_238)) (bvnot (bvlshr ?v_237 ?v_239)) (bvlshr ?v_238 ?v_239)))))) (let ((?v_241 (bvnot ?v_240)) (?v_242 ((_ zero_extend 121) (_ bv81 7)))) (let ((?v_243 (bvand ?v_240 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_241)) (bvnot (bvlshr ?v_240 ?v_242)) (bvlshr ?v_241 ?v_242)))))) (let ((?v_244 (bvnot ?v_243)) (?v_245 ((_ zero_extend 121) (_ bv82 7)))) (let ((?v_246 (bvand ?v_243 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_244)) (bvnot (bvlshr ?v_243 ?v_245)) (bvlshr ?v_244 ?v_245)))))) (let ((?v_247 (bvnot ?v_246)) (?v_248 ((_ zero_extend 121) (_ bv83 7)))) (let ((?v_249 (bvand ?v_246 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_247)) (bvnot (bvlshr ?v_246 ?v_248)) (bvlshr ?v_247 ?v_248)))))) (let ((?v_250 (bvnot ?v_249)) (?v_251 ((_ zero_extend 121) (_ bv84 7)))) (let ((?v_252 (bvand ?v_249 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_250)) (bvnot (bvlshr ?v_249 ?v_251)) (bvlshr ?v_250 ?v_251)))))) (let ((?v_253 (bvnot ?v_252)) (?v_254 ((_ zero_extend 121) (_ bv85 7)))) (let ((?v_255 (bvand ?v_252 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_253)) (bvnot (bvlshr ?v_252 ?v_254)) (bvlshr ?v_253 ?v_254)))))) (let ((?v_256 (bvnot ?v_255)) (?v_257 ((_ zero_extend 121) (_ bv86 7)))) (let ((?v_258 (bvand ?v_255 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_256)) (bvnot (bvlshr ?v_255 ?v_257)) (bvlshr ?v_256 ?v_257)))))) (let ((?v_259 (bvnot ?v_258)) (?v_260 ((_ zero_extend 121) (_ bv87 7)))) (let ((?v_261 (bvand ?v_258 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_259)) (bvnot (bvlshr ?v_258 ?v_260)) (bvlshr ?v_259 ?v_260)))))) (let ((?v_262 (bvnot ?v_261)) (?v_263 ((_ zero_extend 121) (_ bv88 7)))) (let ((?v_264 (bvand ?v_261 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_262)) (bvnot (bvlshr ?v_261 ?v_263)) (bvlshr ?v_262 ?v_263)))))) (let ((?v_265 (bvnot ?v_264)) (?v_266 ((_ zero_extend 121) (_ bv89 7)))) (let ((?v_267 (bvand ?v_264 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_265)) (bvnot (bvlshr ?v_264 ?v_266)) (bvlshr ?v_265 ?v_266)))))) (let ((?v_268 (bvnot ?v_267)) (?v_269 ((_ zero_extend 121) (_ bv90 7)))) (let ((?v_270 (bvand ?v_267 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_268)) (bvnot (bvlshr ?v_267 ?v_269)) (bvlshr ?v_268 ?v_269)))))) (let ((?v_271 (bvnot ?v_270)) (?v_272 ((_ zero_extend 121) (_ bv91 7)))) (let ((?v_273 (bvand ?v_270 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_271)) (bvnot (bvlshr ?v_270 ?v_272)) (bvlshr ?v_271 ?v_272)))))) (let ((?v_274 (bvnot ?v_273)) (?v_275 ((_ zero_extend 121) (_ bv92 7)))) (let ((?v_276 (bvand ?v_273 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_274)) (bvnot (bvlshr ?v_273 ?v_275)) (bvlshr ?v_274 ?v_275)))))) (let ((?v_277 (bvnot ?v_276)) (?v_278 ((_ zero_extend 121) (_ bv93 7)))) (let ((?v_279 (bvand ?v_276 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_277)) (bvnot (bvlshr ?v_276 ?v_278)) (bvlshr ?v_277 ?v_278)))))) (let ((?v_280 (bvnot ?v_279)) (?v_281 ((_ zero_extend 121) (_ bv94 7)))) (let ((?v_282 (bvand ?v_279 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_280)) (bvnot (bvlshr ?v_279 ?v_281)) (bvlshr ?v_280 ?v_281)))))) (let ((?v_283 (bvnot ?v_282)) (?v_284 ((_ zero_extend 121) (_ bv95 7)))) (let ((?v_285 (bvand ?v_282 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_283)) (bvnot (bvlshr ?v_282 ?v_284)) (bvlshr ?v_283 ?v_284)))))) (let ((?v_286 (bvnot ?v_285)) (?v_287 ((_ zero_extend 121) (_ bv96 7)))) (let ((?v_288 (bvand ?v_285 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_286)) (bvnot (bvlshr ?v_285 ?v_287)) (bvlshr ?v_286 ?v_287)))))) (let ((?v_289 (bvnot ?v_288)) (?v_290 ((_ zero_extend 121) (_ bv97 7)))) (let ((?v_291 (bvand ?v_288 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_289)) (bvnot (bvlshr ?v_288 ?v_290)) (bvlshr ?v_289 ?v_290)))))) (let ((?v_292 (bvnot ?v_291)) (?v_293 ((_ zero_extend 121) (_ bv98 7)))) (let ((?v_294 (bvand ?v_291 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_292)) (bvnot (bvlshr ?v_291 ?v_293)) (bvlshr ?v_292 ?v_293)))))) (let ((?v_295 (bvnot ?v_294)) (?v_296 ((_ zero_extend 121) (_ bv99 7)))) (let ((?v_297 (bvand ?v_294 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_295)) (bvnot (bvlshr ?v_294 ?v_296)) (bvlshr ?v_295 ?v_296)))))) (let ((?v_298 (bvnot ?v_297)) (?v_299 ((_ zero_extend 121) (_ bv100 7)))) (let ((?v_300 (bvand ?v_297 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_298)) (bvnot (bvlshr ?v_297 ?v_299)) (bvlshr ?v_298 ?v_299)))))) (let ((?v_301 (bvnot ?v_300)) (?v_302 ((_ zero_extend 121) (_ bv101 7)))) (let ((?v_303 (bvand ?v_300 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_301)) (bvnot (bvlshr ?v_300 ?v_302)) (bvlshr ?v_301 ?v_302)))))) (let ((?v_304 (bvnot ?v_303)) (?v_305 ((_ zero_extend 121) (_ bv102 7)))) (let ((?v_306 (bvand ?v_303 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_304)) (bvnot (bvlshr ?v_303 ?v_305)) (bvlshr ?v_304 ?v_305)))))) (let ((?v_307 (bvnot ?v_306)) (?v_308 ((_ zero_extend 121) (_ bv103 7)))) (let ((?v_309 (bvand ?v_306 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_307)) (bvnot (bvlshr ?v_306 ?v_308)) (bvlshr ?v_307 ?v_308)))))) (let ((?v_310 (bvnot ?v_309)) (?v_311 ((_ zero_extend 121) (_ bv104 7)))) (let ((?v_312 (bvand ?v_309 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_310)) (bvnot (bvlshr ?v_309 ?v_311)) (bvlshr ?v_310 ?v_311)))))) (let ((?v_313 (bvnot ?v_312)) (?v_314 ((_ zero_extend 121) (_ bv105 7)))) (let ((?v_315 (bvand ?v_312 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_313)) (bvnot (bvlshr ?v_312 ?v_314)) (bvlshr ?v_313 ?v_314)))))) (let ((?v_316 (bvnot ?v_315)) (?v_317 ((_ zero_extend 121) (_ bv106 7)))) (let ((?v_318 (bvand ?v_315 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_316)) (bvnot (bvlshr ?v_315 ?v_317)) (bvlshr ?v_316 ?v_317)))))) (let ((?v_319 (bvnot ?v_318)) (?v_320 ((_ zero_extend 121) (_ bv107 7)))) (let ((?v_321 (bvand ?v_318 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_319)) (bvnot (bvlshr ?v_318 ?v_320)) (bvlshr ?v_319 ?v_320)))))) (let ((?v_322 (bvnot ?v_321)) (?v_323 ((_ zero_extend 121) (_ bv108 7)))) (let ((?v_324 (bvand ?v_321 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_322)) (bvnot (bvlshr ?v_321 ?v_323)) (bvlshr ?v_322 ?v_323)))))) (let ((?v_325 (bvnot ?v_324)) (?v_326 ((_ zero_extend 121) (_ bv109 7)))) (let ((?v_327 (bvand ?v_324 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_325)) (bvnot (bvlshr ?v_324 ?v_326)) (bvlshr ?v_325 ?v_326)))))) (let ((?v_328 (bvnot ?v_327)) (?v_329 ((_ zero_extend 121) (_ bv110 7)))) (let ((?v_330 (bvand ?v_327 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_328)) (bvnot (bvlshr ?v_327 ?v_329)) (bvlshr ?v_328 ?v_329)))))) (let ((?v_331 (bvnot ?v_330)) (?v_332 ((_ zero_extend 121) (_ bv111 7)))) (let ((?v_333 (bvand ?v_330 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_331)) (bvnot (bvlshr ?v_330 ?v_332)) (bvlshr ?v_331 ?v_332)))))) (let ((?v_334 (bvnot ?v_333)) (?v_335 ((_ zero_extend 121) (_ bv112 7)))) (let ((?v_336 (bvand ?v_333 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_334)) (bvnot (bvlshr ?v_333 ?v_335)) (bvlshr ?v_334 ?v_335)))))) (let ((?v_337 (bvnot ?v_336)) (?v_338 ((_ zero_extend 121) (_ bv113 7)))) (let ((?v_339 (bvand ?v_336 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_337)) (bvnot (bvlshr ?v_336 ?v_338)) (bvlshr ?v_337 ?v_338)))))) (let ((?v_340 (bvnot ?v_339)) (?v_341 ((_ zero_extend 121) (_ bv114 7)))) (let ((?v_342 (bvand ?v_339 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_340)) (bvnot (bvlshr ?v_339 ?v_341)) (bvlshr ?v_340 ?v_341)))))) (let ((?v_343 (bvnot ?v_342)) (?v_344 ((_ zero_extend 121) (_ bv115 7)))) (let ((?v_345 (bvand ?v_342 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_343)) (bvnot (bvlshr ?v_342 ?v_344)) (bvlshr ?v_343 ?v_344)))))) (let ((?v_346 (bvnot ?v_345)) (?v_347 ((_ zero_extend 121) (_ bv116 7)))) (let ((?v_348 (bvand ?v_345 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_346)) (bvnot (bvlshr ?v_345 ?v_347)) (bvlshr ?v_346 ?v_347)))))) (let ((?v_349 (bvnot ?v_348)) (?v_350 ((_ zero_extend 121) (_ bv117 7)))) (let ((?v_351 (bvand ?v_348 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_349)) (bvnot (bvlshr ?v_348 ?v_350)) (bvlshr ?v_349 ?v_350)))))) (let ((?v_352 (bvnot ?v_351)) (?v_353 ((_ zero_extend 121) (_ bv118 7)))) (let ((?v_354 (bvand ?v_351 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_352)) (bvnot (bvlshr ?v_351 ?v_353)) (bvlshr ?v_352 ?v_353)))))) (let ((?v_355 (bvnot ?v_354)) (?v_356 ((_ zero_extend 121) (_ bv119 7)))) (let ((?v_357 (bvand ?v_354 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_355)) (bvnot (bvlshr ?v_354 ?v_356)) (bvlshr ?v_355 ?v_356)))))) (let ((?v_358 (bvnot ?v_357)) (?v_359 ((_ zero_extend 121) (_ bv120 7)))) (let ((?v_360 (bvand ?v_357 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_358)) (bvnot (bvlshr ?v_357 ?v_359)) (bvlshr ?v_358 ?v_359)))))) (let ((?v_361 (bvnot ?v_360)) (?v_362 ((_ zero_extend 121) (_ bv121 7)))) (let ((?v_363 (bvand ?v_360 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_361)) (bvnot (bvlshr ?v_360 ?v_362)) (bvlshr ?v_361 ?v_362)))))) (let ((?v_364 (bvnot ?v_363)) (?v_365 ((_ zero_extend 121) (_ bv122 7)))) (let ((?v_366 (bvand ?v_363 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_364)) (bvnot (bvlshr ?v_363 ?v_365)) (bvlshr ?v_364 ?v_365)))))) (let ((?v_367 (bvnot ?v_366)) (?v_368 ((_ zero_extend 121) (_ bv123 7)))) (let ((?v_369 (bvand ?v_366 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_367)) (bvnot (bvlshr ?v_366 ?v_368)) (bvlshr ?v_367 ?v_368)))))) (let ((?v_370 (bvnot ?v_369)) (?v_371 ((_ zero_extend 121) (_ bv124 7)))) (let ((?v_372 (bvand ?v_369 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_370)) (bvnot (bvlshr ?v_369 ?v_371)) (bvlshr ?v_370 ?v_371)))))) (let ((?v_373 (bvnot ?v_372)) (?v_374 ((_ zero_extend 121) (_ bv125 7)))) (let ((?v_375 (bvand ?v_372 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_373)) (bvnot (bvlshr ?v_372 ?v_374)) (bvlshr ?v_373 ?v_374)))))) (let ((?v_376 (bvnot ?v_375)) (?v_377 ((_ zero_extend 121) (_ bv126 7)))) (let ((?v_378 (bvand ?v_375 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_376)) (bvnot (bvlshr ?v_375 ?v_377)) (bvlshr ?v_376 ?v_377)))))) (let ((?v_379 (bvnot ?v_378)) (?v_380 ((_ zero_extend 121) (_ bv127 7)))) (let ((?v_381 (bvadd (_ bv1 128) (bvnot (bvand ?v_378 (bvnot (ite (= (_ bv1 1) ((_ extract 127 127) ?v_379)) (bvnot (bvlshr ?v_378 ?v_380)) (bvlshr ?v_379 ?v_380)))))))) (let ((?v_382 (bvlshr ?v_381 ?v_2))) (let ((?v_383 ((_ extract 127 127) ?v_382)) (?v_386 ((_ extract 127 127) x)) (?v_387 ((_ extract 126 0) x))) (let ((?v_385 (ite (bvult ((_ extract 126 0) ?v_382) ?v_387) (_ bv1 1) (_ bv0 1))) (?v_384 (bvnot ?v_386)) (?v_390 ((_ extract 127 127) (_ bv1 128))) (?v_389 (ite (bvult ?v_387 ((_ extract 126 0) (_ bv1 128))) (_ bv1 1) (_ bv0 1)))) (let ((?v_388 (bvnot ?v_390))) (not (= (bvand (bvnot (bvand (bvand (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvnot (_ bv0 1)) (bvnot (ite (= (_ bv1 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv8 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv16 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv32 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv64 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv128 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv256 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv512 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1024 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2048 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4096 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv8192 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv16384 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv32768 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv65536 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv131072 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv262144 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv524288 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1048576 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2097152 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4194304 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv8388608 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv16777216 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv33554432 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv67108864 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv134217728 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv268435456 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv536870912 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1073741824 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2147483648 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4294967296 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv8589934592 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv17179869184 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv34359738368 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv68719476736 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv137438953472 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv274877906944 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv549755813888 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1099511627776 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2199023255552 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4398046511104 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv8796093022208 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv17592186044416 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv35184372088832 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv70368744177664 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv140737488355328 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv281474976710656 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv562949953421312 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1125899906842624 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2251799813685248 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4503599627370496 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv9007199254740992 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv18014398509481984 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv36028797018963968 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv72057594037927936 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv144115188075855872 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv288230376151711744 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv576460752303423488 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1152921504606846976 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2305843009213693952 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4611686018427387904 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv9223372036854775808 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv18446744073709551616 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv36893488147419103232 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv73786976294838206464 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv147573952589676412928 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv295147905179352825856 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv590295810358705651712 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1180591620717411303424 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2361183241434822606848 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4722366482869645213696 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv9444732965739290427392 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv18889465931478580854784 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv37778931862957161709568 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv75557863725914323419136 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv151115727451828646838272 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv302231454903657293676544 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv604462909807314587353088 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1208925819614629174706176 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2417851639229258349412352 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4835703278458516698824704 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv9671406556917033397649408 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv19342813113834066795298816 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv38685626227668133590597632 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv77371252455336267181195264 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv154742504910672534362390528 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv309485009821345068724781056 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv618970019642690137449562112 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1237940039285380274899124224 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2475880078570760549798248448 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4951760157141521099596496896 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv9903520314283042199192993792 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv19807040628566084398385987584 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv39614081257132168796771975168 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv79228162514264337593543950336 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv158456325028528675187087900672 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv316912650057057350374175801344 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv633825300114114700748351602688 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1267650600228229401496703205376 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2535301200456458802993406410752 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv5070602400912917605986812821504 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv10141204801825835211973625643008 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv20282409603651670423947251286016 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv40564819207303340847894502572032 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv81129638414606681695789005144064 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv162259276829213363391578010288128 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv324518553658426726783156020576256 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv649037107316853453566312041152512 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1298074214633706907132624082305024 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2596148429267413814265248164610048 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv5192296858534827628530496329220096 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv10384593717069655257060992658440192 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv20769187434139310514121985316880384 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv41538374868278621028243970633760768 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv83076749736557242056487941267521536 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv166153499473114484112975882535043072 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv332306998946228968225951765070086144 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv664613997892457936451903530140172288 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1329227995784915872903807060280344576 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2658455991569831745807614120560689152 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv5316911983139663491615228241121378304 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv10633823966279326983230456482242756608 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv21267647932558653966460912964485513216 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv42535295865117307932921825928971026432 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv85070591730234615865843651857942052864 128) ?v_381) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv170141183460469231731687303715884105728 128) ?v_381) (_ bv1 1) (_ bv0 1))))) (bvnot (ite (bvult ?v_381 x) (_ bv1 1) (_ bv0 1)))) (bvnot (bvand (bvnot (bvand ?v_383 ?v_384)) (bvand (bvnot (bvand ?v_385 (bvand (bvnot ?v_383) ?v_384))) (bvnot (bvand ?v_385 (bvand ?v_383 ?v_386)))))))) (bvand (bvnot (bvand ?v_386 ?v_388)) (bvand (bvnot (bvand ?v_389 (bvand ?v_384 ?v_388))) (bvnot (bvand ?v_389 (bvand ?v_386 ?v_390)))))) (_ bv0 1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
